{
 "cells": [
  {
   "cell_type": "markdown",
   "id": "1d3b73c1-c30b-4dc4-b2c0-21d47601b09a",
   "metadata": {},
   "source": [
    "# A Large 3-SAT Grover search Example"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "id": "dda1a10d-406f-45f2-9431-13df855375de",
   "metadata": {
    "ExecuteTime": {
     "end_time": "2023-12-31T14:46:58.390448Z",
     "start_time": "2023-12-31T14:46:58.386152Z"
    },
    "execution": {
     "iopub.execute_input": "2024-05-07T14:30:12.467067Z",
     "iopub.status.busy": "2024-05-07T14:30:12.465889Z",
     "iopub.status.idle": "2024-05-07T14:30:12.474998Z",
     "shell.execute_reply": "2024-05-07T14:30:12.474327Z"
    },
    "pycharm": {
     "name": "#%%\n"
    },
    "tags": []
   },
   "outputs": [],
   "source": [
    "EXPRESSION = \"\"\"\n",
    "((x2) or (x3) or (x4)) and\n",
    "((not x1) or ( x2) or ( x3)) and\n",
    "((not x1) or ( x2) or (not x3)) and\n",
    "((not x1) or (not x2) or ( x3)) and\n",
    "(( x1) or (not x2) or (not x3)) and\n",
    "(( x1) or (not x2) or ( x3)) and\n",
    "((not x1) or (not x2) or (not x4)) and\n",
    "((not x1) or (not x2) or ( x4)) and\n",
    "((not x2) or (not x3) or (not x4)) and\n",
    "(( x2) or (not x3) or ( x4)) and\n",
    "(( x1) or (not x3) or ( x4)) and\n",
    "(( x1) or (not x2) or (not x4)) and\n",
    "((not x1) or (not x2) or (not x3))\n",
    "\"\"\""
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "id": "275764e8-46cf-4a7e-9aae-3c5b00ed4f2e",
   "metadata": {
    "execution": {
     "iopub.execute_input": "2024-05-07T14:30:12.479101Z",
     "iopub.status.busy": "2024-05-07T14:30:12.478344Z",
     "iopub.status.idle": "2024-05-07T14:30:12.485344Z",
     "shell.execute_reply": "2024-05-07T14:30:12.484641Z"
    },
    "pycharm": {
     "name": "#%%\n"
    },
    "tags": []
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Please import 'truth-table-generator' in order to print the truth table\n"
     ]
    }
   ],
   "source": [
    "try:\n",
    "    import ttg\n",
    "\n",
    "    print(\n",
    "        ttg.Truths(\n",
    "            [\"x1\", \"x2\", \"x3\", \"x4\"],\n",
    "            [EXPRESSION[1:-1]],\n",
    "        )\n",
    "    )\n",
    "except:\n",
    "    print(\"Please import 'truth-table-generator' in order to print the truth table\")"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "eb39373c-7b72-4a8f-a77b-29bdbf6ebf84",
   "metadata": {
    "tags": []
   },
   "source": [
    "## Loading the model"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "id": "fa7b75cc-5648-435c-9078-e25742f700d5",
   "metadata": {
    "execution": {
     "iopub.execute_input": "2024-05-07T14:30:12.489814Z",
     "iopub.status.busy": "2024-05-07T14:30:12.488622Z",
     "iopub.status.idle": "2024-05-07T14:30:15.441317Z",
     "shell.execute_reply": "2024-05-07T14:30:15.440664Z"
    },
    "pycharm": {
     "name": "#%%\n"
    },
    "tags": []
   },
   "outputs": [],
   "source": [
    "from classiq import RegisterUserInput, construct_grover_model\n",
    "\n",
    "register_size = RegisterUserInput(size=1)\n",
    "\n",
    "qmod = construct_grover_model(\n",
    "    num_reps=1,\n",
    "    expression=\"(\" + EXPRESSION + \")\",\n",
    "    definitions=[\n",
    "        (\"x1\", register_size),\n",
    "        (\"x2\", register_size),\n",
    "        (\"x3\", register_size),\n",
    "        (\"x4\", register_size),\n",
    "    ],\n",
    ")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "id": "37a941d9-e9e3-4b96-84ca-15314398fd76",
   "metadata": {
    "execution": {
     "iopub.execute_input": "2024-05-07T14:30:15.444251Z",
     "iopub.status.busy": "2024-05-07T14:30:15.443636Z",
     "iopub.status.idle": "2024-05-07T14:30:15.454769Z",
     "shell.execute_reply": "2024-05-07T14:30:15.454190Z"
    }
   },
   "outputs": [],
   "source": [
    "from classiq import write_qmod\n",
    "\n",
    "write_qmod(qmod, \"3_sat_grover_large\")"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "2cae9260-cb5a-46a3-9f03-d958e843e688",
   "metadata": {
    "pycharm": {
     "name": "#%% md\n"
    }
   },
   "source": [
    "## Synthesizing the Circuit\n",
    "\n",
    "We proceed by synthesizing the circuit using Classiq's synthesis engine. The synthesis should take approximately several seconds:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "id": "fe260047-cf2f-4a6e-a536-aa3965c57dc2",
   "metadata": {
    "execution": {
     "iopub.execute_input": "2024-05-07T14:30:15.457348Z",
     "iopub.status.busy": "2024-05-07T14:30:15.457174Z",
     "iopub.status.idle": "2024-05-07T14:30:19.946330Z",
     "shell.execute_reply": "2024-05-07T14:30:19.945549Z"
    },
    "tags": []
   },
   "outputs": [],
   "source": [
    "from classiq import QuantumProgram, synthesize\n",
    "\n",
    "qprog = synthesize(qmod)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "99145271-ec09-494d-8c3a-75c3fd24a066",
   "metadata": {
    "pycharm": {
     "name": "#%% md\n"
    },
    "tags": []
   },
   "source": [
    "## Showing the Resulting Circuit\n",
    "\n",
    "After Classiq's synthesis engine has finished the job, we can show the resulting circuit in the interactive GUI:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "id": "ec6fee5b-8d56-4a5e-9db2-f8c7bb3f9fe7",
   "metadata": {
    "execution": {
     "iopub.execute_input": "2024-05-07T14:30:19.951391Z",
     "iopub.status.busy": "2024-05-07T14:30:19.950193Z",
     "iopub.status.idle": "2024-05-07T14:30:20.542044Z",
     "shell.execute_reply": "2024-05-07T14:30:20.541308Z"
    },
    "tags": []
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Opening: https://platform.classiq.io/circuit/dba01c4b-bf9c-49cb-baaf-b726d72d3039?version=0.41.0.dev39%2B79c8fd0855\n"
     ]
    }
   ],
   "source": [
    "circuit = QuantumProgram.from_qprog(qprog)\n",
    "circuit.show()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "id": "d5565dd0-ea9c-4c4b-9f0d-8b9d048a67a9",
   "metadata": {
    "execution": {
     "iopub.execute_input": "2024-05-07T14:30:20.546889Z",
     "iopub.status.busy": "2024-05-07T14:30:20.545649Z",
     "iopub.status.idle": "2024-05-07T14:30:20.552483Z",
     "shell.execute_reply": "2024-05-07T14:30:20.551778Z"
    },
    "pycharm": {
     "name": "#%%\n"
    },
    "tags": []
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "1188\n"
     ]
    }
   ],
   "source": [
    "print(circuit.transpiled_circuit.depth)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "4a071884-a24a-4371-92fb-6525acdcf37e",
   "metadata": {
    "pycharm": {
     "name": "#%% md\n"
    }
   },
   "source": [
    "## Executing the circuit\n",
    "\n",
    "Lastly, we can execute the resulting circuit with Classiq's execute interface, using the `execute` function. We select the number of iterations we wish to run (in this case - 1), and the execution backend (in this case - Classiq's default simulator):"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "id": "d946ca01-dafe-4a69-949f-4a5f6ee1d1ef",
   "metadata": {
    "execution": {
     "iopub.execute_input": "2024-05-07T14:30:20.556983Z",
     "iopub.status.busy": "2024-05-07T14:30:20.555951Z",
     "iopub.status.idle": "2024-05-07T14:30:24.412185Z",
     "shell.execute_reply": "2024-05-07T14:30:24.411534Z"
    },
    "pycharm": {
     "name": "#%%\n"
    },
    "tags": []
   },
   "outputs": [],
   "source": [
    "from classiq import execute, set_quantum_program_execution_preferences\n",
    "from classiq.execution import (\n",
    "    ClassiqBackendPreferences,\n",
    "    ClassiqSimulatorBackendNames,\n",
    "    ExecutionPreferences,\n",
    ")\n",
    "\n",
    "backend_preferences = ExecutionPreferences(\n",
    "    backend_preferences=ClassiqBackendPreferences(\n",
    "        backend_name=ClassiqSimulatorBackendNames.SIMULATOR\n",
    "    )\n",
    ")\n",
    "\n",
    "qprog = set_quantum_program_execution_preferences(qprog, backend_preferences)\n",
    "optimization_result = execute(qprog).result()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "id": "879f6c19-ffa1-47c1-b629-2976914c0249",
   "metadata": {
    "execution": {
     "iopub.execute_input": "2024-05-07T14:30:24.416561Z",
     "iopub.status.busy": "2024-05-07T14:30:24.415500Z",
     "iopub.status.idle": "2024-05-07T14:30:24.419932Z",
     "shell.execute_reply": "2024-05-07T14:30:24.419359Z"
    },
    "tags": []
   },
   "outputs": [],
   "source": [
    "res = optimization_result[0].value"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "6f82191f-2e5b-4c2e-8141-afc31053a45c",
   "metadata": {
    "pycharm": {
     "name": "#%% md\n"
    }
   },
   "source": [
    "Printing out the result, we see that our execution of Grover's algorithm successfully found the satisfying assignments for the input formula with a high probability:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "id": "f0e478c0-1874-427b-b1b8-f9709a38dfab",
   "metadata": {
    "execution": {
     "iopub.execute_input": "2024-05-07T14:30:24.424026Z",
     "iopub.status.busy": "2024-05-07T14:30:24.422881Z",
     "iopub.status.idle": "2024-05-07T14:30:24.434237Z",
     "shell.execute_reply": "2024-05-07T14:30:24.433633Z"
    },
    "tags": []
   },
   "outputs": [
    {
     "data": {
      "text/plain": [
       "{('1', '1', '0', '1'): 20,\n",
       " ('1', '1', '0', '0'): 14,\n",
       " ('1', '1', '1', '0'): 15,\n",
       " ('0', '0', '1', '1'): 361,\n",
       " ('1', '1', '1', '1'): 18,\n",
       " ('1', '0', '0', '0'): 13,\n",
       " ('0', '1', '0', '0'): 11,\n",
       " ('0', '0', '0', '0'): 13,\n",
       " ('0', '0', '1', '0'): 18,\n",
       " ('0', '1', '1', '1'): 15,\n",
       " ('1', '0', '0', '1'): 20,\n",
       " ('1', '0', '1', '0'): 22,\n",
       " ('0', '0', '0', '1'): 411,\n",
       " ('0', '1', '1', '0'): 21,\n",
       " ('1', '0', '1', '1'): 18,\n",
       " ('0', '1', '0', '1'): 10}"
      ]
     },
     "execution_count": 10,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "res.counts_of_multiple_outputs((\"x1\", \"x2\", \"x3\", \"x4\"))"
   ]
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Python 3 (ipykernel)",
   "language": "python",
   "name": "python3"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
   "version": "3.11.9"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 5
}
